Nuprl Lemma : ma-single-frame_wf
0,22
postcript
pdf
x
:Id,
L
:Knd List,
t
:Type. only members of
L
affect
x
:
t
MsgA
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
only members of
L
affect
x
:
t
,
,
f
(
x
)?
z
,
Valtype(
da
;
k
)
,
Prop
,
1of(
t
)
,
x
.
t
(
x
)
,
if
b
t
else
f
fi
,
x
dom(
f
)
,
deq-member(
eq
;
x
;
L
)
,
reduce(
f
;
k
;
as
)
,
false
,
Y
,
x
(
s
)
Lemmas
mk-ma
wf
,
fpf-single
wf
,
Id
wf
,
fpf-empty
wf
,
Knd
wf
,
fpf-cap
wf
,
id-deq
wf
,
ma-state
wf
,
top
wf
,
pi2
wf
,
IdLnk
wf
origin
x:Id, L:Knd List, t:Type. only members of L affect x :t 
MsgA x:Id, L:Knd List, t:Type. only members of L affect x :t MsgA x:A. B(x) T
x. t(x)
t else f fi dom(f)